Playing around with a new Lean4 backend (not based on #2) but rather fresh, adapting the Rocq backend from @DCupello1. Opening this PR to have a place for notes and comments, not meant for merging.

Status

• File generated from NanoWasm is processed successfully.

  make && ./spectec doc/example/NanoWasm.spectec -v -l --lean4 -o Wasm.lean
  

• Files generated from wasm 2.0 are processed successfully.

  git ls-files |entr -c bash -c 'make && ./spectec _specification/wasm-2.0/* -v -l --lean4 -o Wasm.lean'
  

• Files generated from wasm 3.0 are processed successfully (sans definitions)
• Some form of CI is needed
• (Much more to do)

IR-to-IR passes that may be useful

• lifting type alias out of recursive groups

Issues with Lean that we might want to fix or work-around

• deriving DecidableEq for nested inductives (e.g. instr) Support for mutual and nested inductive types as DecidableEq instance generator leanprover/lean4#2329.
  Using BEq so far. (Or maybe we can do away with equality checks on instructions?)

• Nested inductive predicates with indices in parameters Nested inductives cannot have indices leanprover/lean4#1964

  mutual
  inductive Subtype_ok2 : context -> subtype -> oktypeidxnat -> Prop where
    | mk_Subtype_ok2 : forall (C : context) (typeuse_lst : (List typeuse)) (compttype : comptype) (x : idx) (i : Nat) (typeuse'_lst_lst : (List (List typeuse))) (comptype'_lst : (List comptype)) (v_comptype : comptype), 
      Forall (fun (comptype' : comptype) => (Comptype_sub C v_comptype comptype')) comptype'_lst ->
      Subtype_ok2 C (.SUB (some .FINAL) typeuse_lst compttype) (.TYPEIDXNAT_OK x i)
  
  inductive Comptype_sub : context -> comptype -> comptype -> Prop where
  end
  

  This is a big one, as this is a kernel issue. We have two work-arounds:

  • Use the lattice-based construction for predicates that is behind coinduction, and can also do inductives. This can handle that kind of nested recursion.

  • Write

    def Forall (R : α → Prop) : List α → Prop := fun xs => ∀ x ∈ xs, R x
    

    which makes the nested induction go through. Conveniently we already generate xs == ys sie-conditions, so this works easily for Forall₂ as well.